Search Results

Documents authored by Ghica, Dan

Found 2 Possible Name Variants:

Ghica, Dan R.

Document
DOI: 10.4230/LIPIcs.FSCD.2023.14
Rewriting Modulo Traced Comonoid Structure

Authors: Dan R. Ghica and George Kaye

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.
Cite as

Dan R. Ghica and George Kaye. Rewriting Modulo Traced Comonoid Structure. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ghica_et_al:LIPIcs.FSCD.2023.14,
  author =	{Ghica, Dan R. and Kaye, George},
  title =	{{Rewriting Modulo Traced Comonoid Structure}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.14},
  URN =		{urn:nbn:de:0030-drops-179983},
  doi =		{10.4230/LIPIcs.FSCD.2023.14},
  annote =	{Keywords: symmetric traced monoidal categories, string diagrams, graph rewriting, comonoid structure, double pushout rewriting}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Dan R. Ghica and Achim Jung

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ghica_et_al:LIPIcs.CSL.2018.0,
  author =	{Ghica, Dan R. and Jung, Achim},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.0},
  URN =		{urn:nbn:de:0030-drops-96679},
  doi =		{10.4230/LIPIcs.CSL.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.24
Diagrammatic Semantics for Digital Circuits

Authors: Dan R. Ghica, Achim Jung, and Aliaume Lopez

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.
Cite as

Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic Semantics for Digital Circuits. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ghica_et_al:LIPIcs.CSL.2017.24,
  author =	{Ghica, Dan R. and Jung, Achim and Lopez, Aliaume},
  title =	{{Diagrammatic Semantics for Digital Circuits}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.24},
  URN =		{urn:nbn:de:0030-drops-76715},
  doi =		{10.4230/LIPIcs.CSL.2017.24},
  annote =	{Keywords: digital circuits, monoidal categories, string diagrams, rewriting, operational semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.32
The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter

Authors: Koko Muroya and Dan R. Ghica

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming languages. One way is to use abstract machines that pass a token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of abstract machines.
Cite as

Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{muroya_et_al:LIPIcs.CSL.2017.32,
  author =	{Muroya, Koko and Ghica, Dan R.},
  title =	{{The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.32},
  URN =		{urn:nbn:de:0030-drops-76886},
  doi =		{10.4230/LIPIcs.CSL.2017.32},
  annote =	{Keywords: Geometry of Interaction, cost analysis, call-by-need reduction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.374
Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Authors: Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.
Cite as

Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gabbay_et_al:LIPIcs.CSL.2015.374,
  author =	{Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela},
  title =	{{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{374--389},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374},
  URN =		{urn:nbn:de:0030-drops-54262},
  doi =		{10.4230/LIPIcs.CSL.2015.374},
  annote =	{Keywords: nominal sets, scope, alpha equivalence, dynamic sequences}
}

Ghica, Dan

Document
DOI: 10.4230/LIPIcs.CSL.2023.6
Functorial String Diagrams for Reverse-Mode Automatic Differentiation

Authors: Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We formulate a reverse-mode automatic differentiation (RAD) algorithm for (applied) simply typed lambda calculus in the style of Pearlmutter and Siskind [Barak A. Pearlmutter and Jeffrey Mark Siskind, 2008], using the graphical formalism of string diagrams. Thanks to string diagram rewriting, we are able to formally prove for the first time the soundness of such an algorithm. Our approach requires developing a calculus of string diagrams with hierarchical features in the spirit of functorial boxes, in order to model closed monoidal (and cartesian closed) structure. To give an efficient yet principled implementation of the RAD algorithm, we use foliations of our hierarchical string diagrams.
Cite as

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.CSL.2023.6,
  author =	{Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
  title =	{{Functorial String Diagrams for Reverse-Mode Automatic Differentiation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.6},
  URN =		{urn:nbn:de:0030-drops-174674},
  doi =		{10.4230/LIPIcs.CSL.2023.6},
  annote =	{Keywords: string diagrams, automatic differentiation, hierarchical hypergraphs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.37
String Diagrams for Non-Strict Monoidal Categories

Authors: Paul Wilson, Dan Ghica, and Fabio Zanasi

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string diagrams for non-strict monoidal categories, and show how this construction can handle applications in domains such as digital circuits and programming languages. We prove the correctness of our construction, which yields a novel proof of Mac Lane’s strictness theorem. This in turn leads to an elementary graphical proof of Mac Lane’s coherence theorem, and in particular allows for the inductive construction of the canonical isomorphisms in a monoidal category.
Cite as

Paul Wilson, Dan Ghica, and Fabio Zanasi. String Diagrams for Non-Strict Monoidal Categories. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{wilson_et_al:LIPIcs.CSL.2023.37,
  author =	{Wilson, Paul and Ghica, Dan and Zanasi, Fabio},
  title =	{{String Diagrams for Non-Strict Monoidal Categories}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.37},
  URN =		{urn:nbn:de:0030-drops-174981},
  doi =		{10.4230/LIPIcs.CSL.2023.37},
  annote =	{Keywords: String Diagrams, Strictness, Coherence}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.29
Rewriting for Monoidal Closed Categories

Authors: Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
This paper develops a formal string diagram language for monoidal closed categories. Previous work has shown that string diagrams for freely generated symmetric monoidal categories can be viewed as hypergraphs with interfaces, and the axioms of these categories can be realized by rewriting systems. This work proposes hierarchical hypergraphs as a suitable formalization of string diagrams for monoidal closed categories. We then show double pushout rewriting captures the axioms of these closed categories.
Cite as

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Rewriting for Monoidal Closed Categories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.FSCD.2022.29,
  author =	{Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
  title =	{{Rewriting for Monoidal Closed Categories}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.29},
  URN =		{urn:nbn:de:0030-drops-163108},
  doi =		{10.4230/LIPIcs.FSCD.2022.29},
  annote =	{Keywords: string diagrams, rewriting, hierarchical hypergraph, monoidal closed category}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2018
LIPIcs, Volume 119, CSL'18, Complete Volume

Authors: Dan Ghica and Achim Jung

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
LIPIcs, Volume 119, CSL'18, Complete Volume
Cite as

27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Proceedings{ghica_et_al:LIPIcs.CSL.2018,
  title =	{{LIPIcs, Volume 119, CSL'18, Complete Volume}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018},
  URN =		{urn:nbn:de:0030-drops-97444},
  doi =		{10.4230/LIPIcs.CSL.2018},
  annote =	{Keywords: Theory of computation, Software and its engineering, Formal language definitions, Formal software verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact